The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

pairNs → cons(0, n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0, XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Rewrite Strategy: FULL

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair(X, Y), n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

S is empty.
Rewrite Strategy: FULL

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
pair/0
pair/1

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

S is empty.
Rewrite Strategy: FULL

(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(6) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

(7) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
oddNs, incr, activate, repItems

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(8) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

The following defined symbols remain to be analysed:
incr, oddNs, activate, repItems

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol incr.

(10) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

The following defined symbols remain to be analysed:
activate, oddNs, repItems

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Induction Base:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, 0)))

Induction Step:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, +(n11_0, 1)))) →_R^Ω(1)
incr(activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0)))) →_IH
incr(*3_0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(12) Complex Obligation (BEST)

(13) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Lemmas:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

The following defined symbols remain to be analysed:
oddNs, incr, repItems

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol oddNs.

(15) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Lemmas:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

The following defined symbols remain to be analysed:
repItems, incr

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(16) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol repItems.

(17) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Lemmas:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

The following defined symbols remain to be analysed:
incr

They will be analysed ascendingly in the following order:
oddNs = incr
oddNs = activate
oddNs = repItems
incr = activate
incr = repItems
activate = repItems

(18) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol incr.

(19) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Lemmas:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

No more defined symbols left to analyse.

(20) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

(21) BOUNDS(n^1, INF)

(22) Obligation:

TRS:
Rules:
pairNs → cons(0', n__incr(n__oddNs))
oddNs → incr(pairNs)
incr(cons(X, XS)) → cons(s(X), n__incr(activate(XS)))
take(0', XS) → nil
take(s(N), cons(X, XS)) → cons(X, n__take(N, activate(XS)))
zip(nil, XS) → nil
zip(X, nil) → nil
zip(cons(X, XS), cons(Y, YS)) → cons(pair, n__zip(activate(XS), activate(YS)))
tail(cons(X, XS)) → activate(XS)
repItems(nil) → nil
repItems(cons(X, XS)) → cons(X, n__cons(X, n__repItems(activate(XS))))
incr(X) → n__incr(X)
oddNs → n__oddNs
take(X1, X2) → n__take(X1, X2)
zip(X1, X2) → n__zip(X1, X2)
cons(X1, X2) → n__cons(X1, X2)
repItems(X) → n__repItems(X)
activate(n__incr(X)) → incr(activate(X))
activate(n__oddNs) → oddNs
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__zip(X1, X2)) → zip(activate(X1), activate(X2))
activate(n__cons(X1, X2)) → cons(activate(X1), X2)
activate(n__repItems(X)) → repItems(activate(X))
activate(X) → X

Types:
pairNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
0' :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
oddNs :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
incr :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
s :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
activate :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
nil :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__take :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
pair :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__zip :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
tail :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__cons :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
n__repItems :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
hole_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons1_0 :: 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0 :: Nat → 0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons

Lemmas:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

Generator Equations:
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(0) ⇔ 0'
gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(x, 1)) ⇔ n__incr(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
activate(gen_0':n__oddNs:n__incr:s:nil:n__take:pair:n__zip:n__repItems:n__cons2_0(+(1, n11_0))) → *3_0, rt ∈ Ω(n11₀)

(24) BOUNDS(n^1, INF)